(set-logic QF_IDL)
(set-info :source | SMT-COMP'06 Organizers |)
(set-info :smt-lib-version 2.0)
(set-info :category "check")
(set-info :status unsat)
(set-info :notes |This benchmark is designed to check if the DP supports bignumbers.|)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun x3 () Int)
(declare-fun x4 () Int)
(assert (and (<= (- x1 x2) 1000000000000000000000000000000000) (<= (- x2 x3) 2000000000000000000000000000000011) (<= (- x3 x4) (- 1000000000000000000000000000000000)) (<= (- x4 x1) (- 2000000000000000000000000000000012))))
(check-sat)
(exit)
